Definitions | t T, a<b, P  Q, False, A, A B, P & Q, i j < k, , {x:A| B(x) }, , {i..j }, Atom$n, left+right, data(T), x:A B(x), f(a), 1of(t), if b t else f fi, <a,b>, s = t, ||tab|| , x:A B(x), x:A. B(x), #$n, Void, Type, x.A(x),  x. t(x), Prop, True, i j, b,  b, , i< j, T, P  Q, P  Q, Unit, f[x:=v], st-atom(tab;n), encrypt(tab;keyv), secret-table(T), Id, {T}, SQType(T), s ~ t, i= j |